0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 187 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 53 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 239 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 8 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 0 ms)
↳34 QDP
↳35 QDPSizeChangeProof (⇔, 0 ms)
↳36 YES
minusF_in_gaa(0, T25, 0) → minusF_out_gaa(0, T25, 0)
minusF_in_gaa(s(T44), 0, s(T38)) → U12_gaa(T44, T38, minusC_in_ga(T44, T38))
minusC_in_ga(T52, T54) → U5_ga(T52, T54, leD_in_ga(T52, X81))
leD_in_ga(0, true) → leD_out_ga(0, true)
leD_in_ga(s(T60), false) → leD_out_ga(s(T60), false)
U5_ga(T52, T54, leD_out_ga(T52, X81)) → minusC_out_ga(T52, T54)
minusC_in_ga(T68, 0) → U6_ga(T68, leD_in_gg(T68, true))
leD_in_gg(0, true) → leD_out_gg(0, true)
leD_in_gg(s(T60), false) → leD_out_gg(s(T60), false)
U6_ga(T68, leD_out_gg(T68, true)) → minusC_out_ga(T68, 0)
minusC_in_ga(0, s(T75)) → U7_ga(T75, leD_in_gg(0, false))
U7_ga(T75, leD_out_gg(0, false)) → U8_ga(T75, minusA_in_a(T75))
minusA_in_a(T82) → U1_a(T82, leB_in_a(X148))
leB_in_a(true) → leB_out_a(true)
U1_a(T82, leB_out_a(X148)) → minusA_out_a(T82)
minusA_in_a(0) → U2_a(leB_in_g(true))
leB_in_g(true) → leB_out_g(true)
U2_a(leB_out_g(true)) → minusA_out_a(0)
minusA_in_a(s(T87)) → U3_a(T87, leB_in_g(false))
U3_a(T87, leB_out_g(false)) → U4_a(T87, minusA_in_a(T87))
U4_a(T87, minusA_out_a(T87)) → minusA_out_a(s(T87))
U8_ga(T75, minusA_out_a(T75)) → minusC_out_ga(0, s(T75))
minusC_in_ga(s(T94), s(T75)) → U9_ga(T94, T75, leD_in_gg(s(T94), false))
U9_ga(T94, T75, leD_out_gg(s(T94), false)) → U10_ga(T94, T75, minusC_in_ga(T94, T75))
U10_ga(T94, T75, minusC_out_ga(T94, T75)) → minusC_out_ga(s(T94), s(T75))
U12_gaa(T44, T38, minusC_out_ga(T44, T38)) → minusF_out_gaa(s(T44), 0, s(T38))
minusF_in_gaa(s(T101), s(T103), T104) → U13_gaa(T101, T103, T104, leE_in_gaa(T101, T103, X225))
leE_in_gaa(0, T116, true) → leE_out_gaa(0, T116, true)
leE_in_gaa(s(T121), 0, false) → leE_out_gaa(s(T121), 0, false)
leE_in_gaa(s(T126), s(T128), X251) → U11_gaa(T126, T128, X251, leE_in_gaa(T126, T128, X251))
U11_gaa(T126, T128, X251, leE_out_gaa(T126, T128, X251)) → leE_out_gaa(s(T126), s(T128), X251)
U13_gaa(T101, T103, T104, leE_out_gaa(T101, T103, X225)) → minusF_out_gaa(s(T101), s(T103), T104)
minusF_in_gaa(s(T143), s(T144), 0) → U14_gaa(T143, T144, leE_in_gag(T143, T144, true))
leE_in_gag(0, T116, true) → leE_out_gag(0, T116, true)
leE_in_gag(s(T121), 0, false) → leE_out_gag(s(T121), 0, false)
leE_in_gag(s(T126), s(T128), X251) → U11_gag(T126, T128, X251, leE_in_gag(T126, T128, X251))
U11_gag(T126, T128, X251, leE_out_gag(T126, T128, X251)) → leE_out_gag(s(T126), s(T128), X251)
U14_gaa(T143, T144, leE_out_gag(T143, T144, true)) → minusF_out_gaa(s(T143), s(T144), 0)
minusF_in_gaa(s(T163), s(T155), s(T154)) → U15_gaa(T163, T155, T154, leE_in_gag(T163, T155, false))
U15_gaa(T163, T155, T154, leE_out_gag(T163, T155, false)) → U16_gaa(T163, T155, T154, minusF_in_gaa(T163, s(T155), T154))
U16_gaa(T163, T155, T154, minusF_out_gaa(T163, s(T155), T154)) → minusF_out_gaa(s(T163), s(T155), s(T154))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
minusF_in_gaa(0, T25, 0) → minusF_out_gaa(0, T25, 0)
minusF_in_gaa(s(T44), 0, s(T38)) → U12_gaa(T44, T38, minusC_in_ga(T44, T38))
minusC_in_ga(T52, T54) → U5_ga(T52, T54, leD_in_ga(T52, X81))
leD_in_ga(0, true) → leD_out_ga(0, true)
leD_in_ga(s(T60), false) → leD_out_ga(s(T60), false)
U5_ga(T52, T54, leD_out_ga(T52, X81)) → minusC_out_ga(T52, T54)
minusC_in_ga(T68, 0) → U6_ga(T68, leD_in_gg(T68, true))
leD_in_gg(0, true) → leD_out_gg(0, true)
leD_in_gg(s(T60), false) → leD_out_gg(s(T60), false)
U6_ga(T68, leD_out_gg(T68, true)) → minusC_out_ga(T68, 0)
minusC_in_ga(0, s(T75)) → U7_ga(T75, leD_in_gg(0, false))
U7_ga(T75, leD_out_gg(0, false)) → U8_ga(T75, minusA_in_a(T75))
minusA_in_a(T82) → U1_a(T82, leB_in_a(X148))
leB_in_a(true) → leB_out_a(true)
U1_a(T82, leB_out_a(X148)) → minusA_out_a(T82)
minusA_in_a(0) → U2_a(leB_in_g(true))
leB_in_g(true) → leB_out_g(true)
U2_a(leB_out_g(true)) → minusA_out_a(0)
minusA_in_a(s(T87)) → U3_a(T87, leB_in_g(false))
U3_a(T87, leB_out_g(false)) → U4_a(T87, minusA_in_a(T87))
U4_a(T87, minusA_out_a(T87)) → minusA_out_a(s(T87))
U8_ga(T75, minusA_out_a(T75)) → minusC_out_ga(0, s(T75))
minusC_in_ga(s(T94), s(T75)) → U9_ga(T94, T75, leD_in_gg(s(T94), false))
U9_ga(T94, T75, leD_out_gg(s(T94), false)) → U10_ga(T94, T75, minusC_in_ga(T94, T75))
U10_ga(T94, T75, minusC_out_ga(T94, T75)) → minusC_out_ga(s(T94), s(T75))
U12_gaa(T44, T38, minusC_out_ga(T44, T38)) → minusF_out_gaa(s(T44), 0, s(T38))
minusF_in_gaa(s(T101), s(T103), T104) → U13_gaa(T101, T103, T104, leE_in_gaa(T101, T103, X225))
leE_in_gaa(0, T116, true) → leE_out_gaa(0, T116, true)
leE_in_gaa(s(T121), 0, false) → leE_out_gaa(s(T121), 0, false)
leE_in_gaa(s(T126), s(T128), X251) → U11_gaa(T126, T128, X251, leE_in_gaa(T126, T128, X251))
U11_gaa(T126, T128, X251, leE_out_gaa(T126, T128, X251)) → leE_out_gaa(s(T126), s(T128), X251)
U13_gaa(T101, T103, T104, leE_out_gaa(T101, T103, X225)) → minusF_out_gaa(s(T101), s(T103), T104)
minusF_in_gaa(s(T143), s(T144), 0) → U14_gaa(T143, T144, leE_in_gag(T143, T144, true))
leE_in_gag(0, T116, true) → leE_out_gag(0, T116, true)
leE_in_gag(s(T121), 0, false) → leE_out_gag(s(T121), 0, false)
leE_in_gag(s(T126), s(T128), X251) → U11_gag(T126, T128, X251, leE_in_gag(T126, T128, X251))
U11_gag(T126, T128, X251, leE_out_gag(T126, T128, X251)) → leE_out_gag(s(T126), s(T128), X251)
U14_gaa(T143, T144, leE_out_gag(T143, T144, true)) → minusF_out_gaa(s(T143), s(T144), 0)
minusF_in_gaa(s(T163), s(T155), s(T154)) → U15_gaa(T163, T155, T154, leE_in_gag(T163, T155, false))
U15_gaa(T163, T155, T154, leE_out_gag(T163, T155, false)) → U16_gaa(T163, T155, T154, minusF_in_gaa(T163, s(T155), T154))
U16_gaa(T163, T155, T154, minusF_out_gaa(T163, s(T155), T154)) → minusF_out_gaa(s(T163), s(T155), s(T154))
MINUSF_IN_GAA(s(T44), 0, s(T38)) → U12_GAA(T44, T38, minusC_in_ga(T44, T38))
MINUSF_IN_GAA(s(T44), 0, s(T38)) → MINUSC_IN_GA(T44, T38)
MINUSC_IN_GA(T52, T54) → U5_GA(T52, T54, leD_in_ga(T52, X81))
MINUSC_IN_GA(T52, T54) → LED_IN_GA(T52, X81)
MINUSC_IN_GA(T68, 0) → U6_GA(T68, leD_in_gg(T68, true))
MINUSC_IN_GA(T68, 0) → LED_IN_GG(T68, true)
MINUSC_IN_GA(0, s(T75)) → U7_GA(T75, leD_in_gg(0, false))
MINUSC_IN_GA(0, s(T75)) → LED_IN_GG(0, false)
U7_GA(T75, leD_out_gg(0, false)) → U8_GA(T75, minusA_in_a(T75))
U7_GA(T75, leD_out_gg(0, false)) → MINUSA_IN_A(T75)
MINUSA_IN_A(T82) → U1_A(T82, leB_in_a(X148))
MINUSA_IN_A(T82) → LEB_IN_A(X148)
MINUSA_IN_A(0) → U2_A(leB_in_g(true))
MINUSA_IN_A(0) → LEB_IN_G(true)
MINUSA_IN_A(s(T87)) → U3_A(T87, leB_in_g(false))
MINUSA_IN_A(s(T87)) → LEB_IN_G(false)
U3_A(T87, leB_out_g(false)) → U4_A(T87, minusA_in_a(T87))
U3_A(T87, leB_out_g(false)) → MINUSA_IN_A(T87)
MINUSC_IN_GA(s(T94), s(T75)) → U9_GA(T94, T75, leD_in_gg(s(T94), false))
MINUSC_IN_GA(s(T94), s(T75)) → LED_IN_GG(s(T94), false)
U9_GA(T94, T75, leD_out_gg(s(T94), false)) → U10_GA(T94, T75, minusC_in_ga(T94, T75))
U9_GA(T94, T75, leD_out_gg(s(T94), false)) → MINUSC_IN_GA(T94, T75)
MINUSF_IN_GAA(s(T101), s(T103), T104) → U13_GAA(T101, T103, T104, leE_in_gaa(T101, T103, X225))
MINUSF_IN_GAA(s(T101), s(T103), T104) → LEE_IN_GAA(T101, T103, X225)
LEE_IN_GAA(s(T126), s(T128), X251) → U11_GAA(T126, T128, X251, leE_in_gaa(T126, T128, X251))
LEE_IN_GAA(s(T126), s(T128), X251) → LEE_IN_GAA(T126, T128, X251)
MINUSF_IN_GAA(s(T143), s(T144), 0) → U14_GAA(T143, T144, leE_in_gag(T143, T144, true))
MINUSF_IN_GAA(s(T143), s(T144), 0) → LEE_IN_GAG(T143, T144, true)
LEE_IN_GAG(s(T126), s(T128), X251) → U11_GAG(T126, T128, X251, leE_in_gag(T126, T128, X251))
LEE_IN_GAG(s(T126), s(T128), X251) → LEE_IN_GAG(T126, T128, X251)
MINUSF_IN_GAA(s(T163), s(T155), s(T154)) → U15_GAA(T163, T155, T154, leE_in_gag(T163, T155, false))
MINUSF_IN_GAA(s(T163), s(T155), s(T154)) → LEE_IN_GAG(T163, T155, false)
U15_GAA(T163, T155, T154, leE_out_gag(T163, T155, false)) → U16_GAA(T163, T155, T154, minusF_in_gaa(T163, s(T155), T154))
U15_GAA(T163, T155, T154, leE_out_gag(T163, T155, false)) → MINUSF_IN_GAA(T163, s(T155), T154)
minusF_in_gaa(0, T25, 0) → minusF_out_gaa(0, T25, 0)
minusF_in_gaa(s(T44), 0, s(T38)) → U12_gaa(T44, T38, minusC_in_ga(T44, T38))
minusC_in_ga(T52, T54) → U5_ga(T52, T54, leD_in_ga(T52, X81))
leD_in_ga(0, true) → leD_out_ga(0, true)
leD_in_ga(s(T60), false) → leD_out_ga(s(T60), false)
U5_ga(T52, T54, leD_out_ga(T52, X81)) → minusC_out_ga(T52, T54)
minusC_in_ga(T68, 0) → U6_ga(T68, leD_in_gg(T68, true))
leD_in_gg(0, true) → leD_out_gg(0, true)
leD_in_gg(s(T60), false) → leD_out_gg(s(T60), false)
U6_ga(T68, leD_out_gg(T68, true)) → minusC_out_ga(T68, 0)
minusC_in_ga(0, s(T75)) → U7_ga(T75, leD_in_gg(0, false))
U7_ga(T75, leD_out_gg(0, false)) → U8_ga(T75, minusA_in_a(T75))
minusA_in_a(T82) → U1_a(T82, leB_in_a(X148))
leB_in_a(true) → leB_out_a(true)
U1_a(T82, leB_out_a(X148)) → minusA_out_a(T82)
minusA_in_a(0) → U2_a(leB_in_g(true))
leB_in_g(true) → leB_out_g(true)
U2_a(leB_out_g(true)) → minusA_out_a(0)
minusA_in_a(s(T87)) → U3_a(T87, leB_in_g(false))
U3_a(T87, leB_out_g(false)) → U4_a(T87, minusA_in_a(T87))
U4_a(T87, minusA_out_a(T87)) → minusA_out_a(s(T87))
U8_ga(T75, minusA_out_a(T75)) → minusC_out_ga(0, s(T75))
minusC_in_ga(s(T94), s(T75)) → U9_ga(T94, T75, leD_in_gg(s(T94), false))
U9_ga(T94, T75, leD_out_gg(s(T94), false)) → U10_ga(T94, T75, minusC_in_ga(T94, T75))
U10_ga(T94, T75, minusC_out_ga(T94, T75)) → minusC_out_ga(s(T94), s(T75))
U12_gaa(T44, T38, minusC_out_ga(T44, T38)) → minusF_out_gaa(s(T44), 0, s(T38))
minusF_in_gaa(s(T101), s(T103), T104) → U13_gaa(T101, T103, T104, leE_in_gaa(T101, T103, X225))
leE_in_gaa(0, T116, true) → leE_out_gaa(0, T116, true)
leE_in_gaa(s(T121), 0, false) → leE_out_gaa(s(T121), 0, false)
leE_in_gaa(s(T126), s(T128), X251) → U11_gaa(T126, T128, X251, leE_in_gaa(T126, T128, X251))
U11_gaa(T126, T128, X251, leE_out_gaa(T126, T128, X251)) → leE_out_gaa(s(T126), s(T128), X251)
U13_gaa(T101, T103, T104, leE_out_gaa(T101, T103, X225)) → minusF_out_gaa(s(T101), s(T103), T104)
minusF_in_gaa(s(T143), s(T144), 0) → U14_gaa(T143, T144, leE_in_gag(T143, T144, true))
leE_in_gag(0, T116, true) → leE_out_gag(0, T116, true)
leE_in_gag(s(T121), 0, false) → leE_out_gag(s(T121), 0, false)
leE_in_gag(s(T126), s(T128), X251) → U11_gag(T126, T128, X251, leE_in_gag(T126, T128, X251))
U11_gag(T126, T128, X251, leE_out_gag(T126, T128, X251)) → leE_out_gag(s(T126), s(T128), X251)
U14_gaa(T143, T144, leE_out_gag(T143, T144, true)) → minusF_out_gaa(s(T143), s(T144), 0)
minusF_in_gaa(s(T163), s(T155), s(T154)) → U15_gaa(T163, T155, T154, leE_in_gag(T163, T155, false))
U15_gaa(T163, T155, T154, leE_out_gag(T163, T155, false)) → U16_gaa(T163, T155, T154, minusF_in_gaa(T163, s(T155), T154))
U16_gaa(T163, T155, T154, minusF_out_gaa(T163, s(T155), T154)) → minusF_out_gaa(s(T163), s(T155), s(T154))
MINUSF_IN_GAA(s(T44), 0, s(T38)) → U12_GAA(T44, T38, minusC_in_ga(T44, T38))
MINUSF_IN_GAA(s(T44), 0, s(T38)) → MINUSC_IN_GA(T44, T38)
MINUSC_IN_GA(T52, T54) → U5_GA(T52, T54, leD_in_ga(T52, X81))
MINUSC_IN_GA(T52, T54) → LED_IN_GA(T52, X81)
MINUSC_IN_GA(T68, 0) → U6_GA(T68, leD_in_gg(T68, true))
MINUSC_IN_GA(T68, 0) → LED_IN_GG(T68, true)
MINUSC_IN_GA(0, s(T75)) → U7_GA(T75, leD_in_gg(0, false))
MINUSC_IN_GA(0, s(T75)) → LED_IN_GG(0, false)
U7_GA(T75, leD_out_gg(0, false)) → U8_GA(T75, minusA_in_a(T75))
U7_GA(T75, leD_out_gg(0, false)) → MINUSA_IN_A(T75)
MINUSA_IN_A(T82) → U1_A(T82, leB_in_a(X148))
MINUSA_IN_A(T82) → LEB_IN_A(X148)
MINUSA_IN_A(0) → U2_A(leB_in_g(true))
MINUSA_IN_A(0) → LEB_IN_G(true)
MINUSA_IN_A(s(T87)) → U3_A(T87, leB_in_g(false))
MINUSA_IN_A(s(T87)) → LEB_IN_G(false)
U3_A(T87, leB_out_g(false)) → U4_A(T87, minusA_in_a(T87))
U3_A(T87, leB_out_g(false)) → MINUSA_IN_A(T87)
MINUSC_IN_GA(s(T94), s(T75)) → U9_GA(T94, T75, leD_in_gg(s(T94), false))
MINUSC_IN_GA(s(T94), s(T75)) → LED_IN_GG(s(T94), false)
U9_GA(T94, T75, leD_out_gg(s(T94), false)) → U10_GA(T94, T75, minusC_in_ga(T94, T75))
U9_GA(T94, T75, leD_out_gg(s(T94), false)) → MINUSC_IN_GA(T94, T75)
MINUSF_IN_GAA(s(T101), s(T103), T104) → U13_GAA(T101, T103, T104, leE_in_gaa(T101, T103, X225))
MINUSF_IN_GAA(s(T101), s(T103), T104) → LEE_IN_GAA(T101, T103, X225)
LEE_IN_GAA(s(T126), s(T128), X251) → U11_GAA(T126, T128, X251, leE_in_gaa(T126, T128, X251))
LEE_IN_GAA(s(T126), s(T128), X251) → LEE_IN_GAA(T126, T128, X251)
MINUSF_IN_GAA(s(T143), s(T144), 0) → U14_GAA(T143, T144, leE_in_gag(T143, T144, true))
MINUSF_IN_GAA(s(T143), s(T144), 0) → LEE_IN_GAG(T143, T144, true)
LEE_IN_GAG(s(T126), s(T128), X251) → U11_GAG(T126, T128, X251, leE_in_gag(T126, T128, X251))
LEE_IN_GAG(s(T126), s(T128), X251) → LEE_IN_GAG(T126, T128, X251)
MINUSF_IN_GAA(s(T163), s(T155), s(T154)) → U15_GAA(T163, T155, T154, leE_in_gag(T163, T155, false))
MINUSF_IN_GAA(s(T163), s(T155), s(T154)) → LEE_IN_GAG(T163, T155, false)
U15_GAA(T163, T155, T154, leE_out_gag(T163, T155, false)) → U16_GAA(T163, T155, T154, minusF_in_gaa(T163, s(T155), T154))
U15_GAA(T163, T155, T154, leE_out_gag(T163, T155, false)) → MINUSF_IN_GAA(T163, s(T155), T154)
minusF_in_gaa(0, T25, 0) → minusF_out_gaa(0, T25, 0)
minusF_in_gaa(s(T44), 0, s(T38)) → U12_gaa(T44, T38, minusC_in_ga(T44, T38))
minusC_in_ga(T52, T54) → U5_ga(T52, T54, leD_in_ga(T52, X81))
leD_in_ga(0, true) → leD_out_ga(0, true)
leD_in_ga(s(T60), false) → leD_out_ga(s(T60), false)
U5_ga(T52, T54, leD_out_ga(T52, X81)) → minusC_out_ga(T52, T54)
minusC_in_ga(T68, 0) → U6_ga(T68, leD_in_gg(T68, true))
leD_in_gg(0, true) → leD_out_gg(0, true)
leD_in_gg(s(T60), false) → leD_out_gg(s(T60), false)
U6_ga(T68, leD_out_gg(T68, true)) → minusC_out_ga(T68, 0)
minusC_in_ga(0, s(T75)) → U7_ga(T75, leD_in_gg(0, false))
U7_ga(T75, leD_out_gg(0, false)) → U8_ga(T75, minusA_in_a(T75))
minusA_in_a(T82) → U1_a(T82, leB_in_a(X148))
leB_in_a(true) → leB_out_a(true)
U1_a(T82, leB_out_a(X148)) → minusA_out_a(T82)
minusA_in_a(0) → U2_a(leB_in_g(true))
leB_in_g(true) → leB_out_g(true)
U2_a(leB_out_g(true)) → minusA_out_a(0)
minusA_in_a(s(T87)) → U3_a(T87, leB_in_g(false))
U3_a(T87, leB_out_g(false)) → U4_a(T87, minusA_in_a(T87))
U4_a(T87, minusA_out_a(T87)) → minusA_out_a(s(T87))
U8_ga(T75, minusA_out_a(T75)) → minusC_out_ga(0, s(T75))
minusC_in_ga(s(T94), s(T75)) → U9_ga(T94, T75, leD_in_gg(s(T94), false))
U9_ga(T94, T75, leD_out_gg(s(T94), false)) → U10_ga(T94, T75, minusC_in_ga(T94, T75))
U10_ga(T94, T75, minusC_out_ga(T94, T75)) → minusC_out_ga(s(T94), s(T75))
U12_gaa(T44, T38, minusC_out_ga(T44, T38)) → minusF_out_gaa(s(T44), 0, s(T38))
minusF_in_gaa(s(T101), s(T103), T104) → U13_gaa(T101, T103, T104, leE_in_gaa(T101, T103, X225))
leE_in_gaa(0, T116, true) → leE_out_gaa(0, T116, true)
leE_in_gaa(s(T121), 0, false) → leE_out_gaa(s(T121), 0, false)
leE_in_gaa(s(T126), s(T128), X251) → U11_gaa(T126, T128, X251, leE_in_gaa(T126, T128, X251))
U11_gaa(T126, T128, X251, leE_out_gaa(T126, T128, X251)) → leE_out_gaa(s(T126), s(T128), X251)
U13_gaa(T101, T103, T104, leE_out_gaa(T101, T103, X225)) → minusF_out_gaa(s(T101), s(T103), T104)
minusF_in_gaa(s(T143), s(T144), 0) → U14_gaa(T143, T144, leE_in_gag(T143, T144, true))
leE_in_gag(0, T116, true) → leE_out_gag(0, T116, true)
leE_in_gag(s(T121), 0, false) → leE_out_gag(s(T121), 0, false)
leE_in_gag(s(T126), s(T128), X251) → U11_gag(T126, T128, X251, leE_in_gag(T126, T128, X251))
U11_gag(T126, T128, X251, leE_out_gag(T126, T128, X251)) → leE_out_gag(s(T126), s(T128), X251)
U14_gaa(T143, T144, leE_out_gag(T143, T144, true)) → minusF_out_gaa(s(T143), s(T144), 0)
minusF_in_gaa(s(T163), s(T155), s(T154)) → U15_gaa(T163, T155, T154, leE_in_gag(T163, T155, false))
U15_gaa(T163, T155, T154, leE_out_gag(T163, T155, false)) → U16_gaa(T163, T155, T154, minusF_in_gaa(T163, s(T155), T154))
U16_gaa(T163, T155, T154, minusF_out_gaa(T163, s(T155), T154)) → minusF_out_gaa(s(T163), s(T155), s(T154))
LEE_IN_GAG(s(T126), s(T128), X251) → LEE_IN_GAG(T126, T128, X251)
minusF_in_gaa(0, T25, 0) → minusF_out_gaa(0, T25, 0)
minusF_in_gaa(s(T44), 0, s(T38)) → U12_gaa(T44, T38, minusC_in_ga(T44, T38))
minusC_in_ga(T52, T54) → U5_ga(T52, T54, leD_in_ga(T52, X81))
leD_in_ga(0, true) → leD_out_ga(0, true)
leD_in_ga(s(T60), false) → leD_out_ga(s(T60), false)
U5_ga(T52, T54, leD_out_ga(T52, X81)) → minusC_out_ga(T52, T54)
minusC_in_ga(T68, 0) → U6_ga(T68, leD_in_gg(T68, true))
leD_in_gg(0, true) → leD_out_gg(0, true)
leD_in_gg(s(T60), false) → leD_out_gg(s(T60), false)
U6_ga(T68, leD_out_gg(T68, true)) → minusC_out_ga(T68, 0)
minusC_in_ga(0, s(T75)) → U7_ga(T75, leD_in_gg(0, false))
U7_ga(T75, leD_out_gg(0, false)) → U8_ga(T75, minusA_in_a(T75))
minusA_in_a(T82) → U1_a(T82, leB_in_a(X148))
leB_in_a(true) → leB_out_a(true)
U1_a(T82, leB_out_a(X148)) → minusA_out_a(T82)
minusA_in_a(0) → U2_a(leB_in_g(true))
leB_in_g(true) → leB_out_g(true)
U2_a(leB_out_g(true)) → minusA_out_a(0)
minusA_in_a(s(T87)) → U3_a(T87, leB_in_g(false))
U3_a(T87, leB_out_g(false)) → U4_a(T87, minusA_in_a(T87))
U4_a(T87, minusA_out_a(T87)) → minusA_out_a(s(T87))
U8_ga(T75, minusA_out_a(T75)) → minusC_out_ga(0, s(T75))
minusC_in_ga(s(T94), s(T75)) → U9_ga(T94, T75, leD_in_gg(s(T94), false))
U9_ga(T94, T75, leD_out_gg(s(T94), false)) → U10_ga(T94, T75, minusC_in_ga(T94, T75))
U10_ga(T94, T75, minusC_out_ga(T94, T75)) → minusC_out_ga(s(T94), s(T75))
U12_gaa(T44, T38, minusC_out_ga(T44, T38)) → minusF_out_gaa(s(T44), 0, s(T38))
minusF_in_gaa(s(T101), s(T103), T104) → U13_gaa(T101, T103, T104, leE_in_gaa(T101, T103, X225))
leE_in_gaa(0, T116, true) → leE_out_gaa(0, T116, true)
leE_in_gaa(s(T121), 0, false) → leE_out_gaa(s(T121), 0, false)
leE_in_gaa(s(T126), s(T128), X251) → U11_gaa(T126, T128, X251, leE_in_gaa(T126, T128, X251))
U11_gaa(T126, T128, X251, leE_out_gaa(T126, T128, X251)) → leE_out_gaa(s(T126), s(T128), X251)
U13_gaa(T101, T103, T104, leE_out_gaa(T101, T103, X225)) → minusF_out_gaa(s(T101), s(T103), T104)
minusF_in_gaa(s(T143), s(T144), 0) → U14_gaa(T143, T144, leE_in_gag(T143, T144, true))
leE_in_gag(0, T116, true) → leE_out_gag(0, T116, true)
leE_in_gag(s(T121), 0, false) → leE_out_gag(s(T121), 0, false)
leE_in_gag(s(T126), s(T128), X251) → U11_gag(T126, T128, X251, leE_in_gag(T126, T128, X251))
U11_gag(T126, T128, X251, leE_out_gag(T126, T128, X251)) → leE_out_gag(s(T126), s(T128), X251)
U14_gaa(T143, T144, leE_out_gag(T143, T144, true)) → minusF_out_gaa(s(T143), s(T144), 0)
minusF_in_gaa(s(T163), s(T155), s(T154)) → U15_gaa(T163, T155, T154, leE_in_gag(T163, T155, false))
U15_gaa(T163, T155, T154, leE_out_gag(T163, T155, false)) → U16_gaa(T163, T155, T154, minusF_in_gaa(T163, s(T155), T154))
U16_gaa(T163, T155, T154, minusF_out_gaa(T163, s(T155), T154)) → minusF_out_gaa(s(T163), s(T155), s(T154))
LEE_IN_GAG(s(T126), s(T128), X251) → LEE_IN_GAG(T126, T128, X251)
LEE_IN_GAG(s(T126), X251) → LEE_IN_GAG(T126, X251)
From the DPs we obtained the following set of size-change graphs:
LEE_IN_GAA(s(T126), s(T128), X251) → LEE_IN_GAA(T126, T128, X251)
minusF_in_gaa(0, T25, 0) → minusF_out_gaa(0, T25, 0)
minusF_in_gaa(s(T44), 0, s(T38)) → U12_gaa(T44, T38, minusC_in_ga(T44, T38))
minusC_in_ga(T52, T54) → U5_ga(T52, T54, leD_in_ga(T52, X81))
leD_in_ga(0, true) → leD_out_ga(0, true)
leD_in_ga(s(T60), false) → leD_out_ga(s(T60), false)
U5_ga(T52, T54, leD_out_ga(T52, X81)) → minusC_out_ga(T52, T54)
minusC_in_ga(T68, 0) → U6_ga(T68, leD_in_gg(T68, true))
leD_in_gg(0, true) → leD_out_gg(0, true)
leD_in_gg(s(T60), false) → leD_out_gg(s(T60), false)
U6_ga(T68, leD_out_gg(T68, true)) → minusC_out_ga(T68, 0)
minusC_in_ga(0, s(T75)) → U7_ga(T75, leD_in_gg(0, false))
U7_ga(T75, leD_out_gg(0, false)) → U8_ga(T75, minusA_in_a(T75))
minusA_in_a(T82) → U1_a(T82, leB_in_a(X148))
leB_in_a(true) → leB_out_a(true)
U1_a(T82, leB_out_a(X148)) → minusA_out_a(T82)
minusA_in_a(0) → U2_a(leB_in_g(true))
leB_in_g(true) → leB_out_g(true)
U2_a(leB_out_g(true)) → minusA_out_a(0)
minusA_in_a(s(T87)) → U3_a(T87, leB_in_g(false))
U3_a(T87, leB_out_g(false)) → U4_a(T87, minusA_in_a(T87))
U4_a(T87, minusA_out_a(T87)) → minusA_out_a(s(T87))
U8_ga(T75, minusA_out_a(T75)) → minusC_out_ga(0, s(T75))
minusC_in_ga(s(T94), s(T75)) → U9_ga(T94, T75, leD_in_gg(s(T94), false))
U9_ga(T94, T75, leD_out_gg(s(T94), false)) → U10_ga(T94, T75, minusC_in_ga(T94, T75))
U10_ga(T94, T75, minusC_out_ga(T94, T75)) → minusC_out_ga(s(T94), s(T75))
U12_gaa(T44, T38, minusC_out_ga(T44, T38)) → minusF_out_gaa(s(T44), 0, s(T38))
minusF_in_gaa(s(T101), s(T103), T104) → U13_gaa(T101, T103, T104, leE_in_gaa(T101, T103, X225))
leE_in_gaa(0, T116, true) → leE_out_gaa(0, T116, true)
leE_in_gaa(s(T121), 0, false) → leE_out_gaa(s(T121), 0, false)
leE_in_gaa(s(T126), s(T128), X251) → U11_gaa(T126, T128, X251, leE_in_gaa(T126, T128, X251))
U11_gaa(T126, T128, X251, leE_out_gaa(T126, T128, X251)) → leE_out_gaa(s(T126), s(T128), X251)
U13_gaa(T101, T103, T104, leE_out_gaa(T101, T103, X225)) → minusF_out_gaa(s(T101), s(T103), T104)
minusF_in_gaa(s(T143), s(T144), 0) → U14_gaa(T143, T144, leE_in_gag(T143, T144, true))
leE_in_gag(0, T116, true) → leE_out_gag(0, T116, true)
leE_in_gag(s(T121), 0, false) → leE_out_gag(s(T121), 0, false)
leE_in_gag(s(T126), s(T128), X251) → U11_gag(T126, T128, X251, leE_in_gag(T126, T128, X251))
U11_gag(T126, T128, X251, leE_out_gag(T126, T128, X251)) → leE_out_gag(s(T126), s(T128), X251)
U14_gaa(T143, T144, leE_out_gag(T143, T144, true)) → minusF_out_gaa(s(T143), s(T144), 0)
minusF_in_gaa(s(T163), s(T155), s(T154)) → U15_gaa(T163, T155, T154, leE_in_gag(T163, T155, false))
U15_gaa(T163, T155, T154, leE_out_gag(T163, T155, false)) → U16_gaa(T163, T155, T154, minusF_in_gaa(T163, s(T155), T154))
U16_gaa(T163, T155, T154, minusF_out_gaa(T163, s(T155), T154)) → minusF_out_gaa(s(T163), s(T155), s(T154))
LEE_IN_GAA(s(T126), s(T128), X251) → LEE_IN_GAA(T126, T128, X251)
LEE_IN_GAA(s(T126)) → LEE_IN_GAA(T126)
From the DPs we obtained the following set of size-change graphs:
MINUSF_IN_GAA(s(T163), s(T155), s(T154)) → U15_GAA(T163, T155, T154, leE_in_gag(T163, T155, false))
U15_GAA(T163, T155, T154, leE_out_gag(T163, T155, false)) → MINUSF_IN_GAA(T163, s(T155), T154)
minusF_in_gaa(0, T25, 0) → minusF_out_gaa(0, T25, 0)
minusF_in_gaa(s(T44), 0, s(T38)) → U12_gaa(T44, T38, minusC_in_ga(T44, T38))
minusC_in_ga(T52, T54) → U5_ga(T52, T54, leD_in_ga(T52, X81))
leD_in_ga(0, true) → leD_out_ga(0, true)
leD_in_ga(s(T60), false) → leD_out_ga(s(T60), false)
U5_ga(T52, T54, leD_out_ga(T52, X81)) → minusC_out_ga(T52, T54)
minusC_in_ga(T68, 0) → U6_ga(T68, leD_in_gg(T68, true))
leD_in_gg(0, true) → leD_out_gg(0, true)
leD_in_gg(s(T60), false) → leD_out_gg(s(T60), false)
U6_ga(T68, leD_out_gg(T68, true)) → minusC_out_ga(T68, 0)
minusC_in_ga(0, s(T75)) → U7_ga(T75, leD_in_gg(0, false))
U7_ga(T75, leD_out_gg(0, false)) → U8_ga(T75, minusA_in_a(T75))
minusA_in_a(T82) → U1_a(T82, leB_in_a(X148))
leB_in_a(true) → leB_out_a(true)
U1_a(T82, leB_out_a(X148)) → minusA_out_a(T82)
minusA_in_a(0) → U2_a(leB_in_g(true))
leB_in_g(true) → leB_out_g(true)
U2_a(leB_out_g(true)) → minusA_out_a(0)
minusA_in_a(s(T87)) → U3_a(T87, leB_in_g(false))
U3_a(T87, leB_out_g(false)) → U4_a(T87, minusA_in_a(T87))
U4_a(T87, minusA_out_a(T87)) → minusA_out_a(s(T87))
U8_ga(T75, minusA_out_a(T75)) → minusC_out_ga(0, s(T75))
minusC_in_ga(s(T94), s(T75)) → U9_ga(T94, T75, leD_in_gg(s(T94), false))
U9_ga(T94, T75, leD_out_gg(s(T94), false)) → U10_ga(T94, T75, minusC_in_ga(T94, T75))
U10_ga(T94, T75, minusC_out_ga(T94, T75)) → minusC_out_ga(s(T94), s(T75))
U12_gaa(T44, T38, minusC_out_ga(T44, T38)) → minusF_out_gaa(s(T44), 0, s(T38))
minusF_in_gaa(s(T101), s(T103), T104) → U13_gaa(T101, T103, T104, leE_in_gaa(T101, T103, X225))
leE_in_gaa(0, T116, true) → leE_out_gaa(0, T116, true)
leE_in_gaa(s(T121), 0, false) → leE_out_gaa(s(T121), 0, false)
leE_in_gaa(s(T126), s(T128), X251) → U11_gaa(T126, T128, X251, leE_in_gaa(T126, T128, X251))
U11_gaa(T126, T128, X251, leE_out_gaa(T126, T128, X251)) → leE_out_gaa(s(T126), s(T128), X251)
U13_gaa(T101, T103, T104, leE_out_gaa(T101, T103, X225)) → minusF_out_gaa(s(T101), s(T103), T104)
minusF_in_gaa(s(T143), s(T144), 0) → U14_gaa(T143, T144, leE_in_gag(T143, T144, true))
leE_in_gag(0, T116, true) → leE_out_gag(0, T116, true)
leE_in_gag(s(T121), 0, false) → leE_out_gag(s(T121), 0, false)
leE_in_gag(s(T126), s(T128), X251) → U11_gag(T126, T128, X251, leE_in_gag(T126, T128, X251))
U11_gag(T126, T128, X251, leE_out_gag(T126, T128, X251)) → leE_out_gag(s(T126), s(T128), X251)
U14_gaa(T143, T144, leE_out_gag(T143, T144, true)) → minusF_out_gaa(s(T143), s(T144), 0)
minusF_in_gaa(s(T163), s(T155), s(T154)) → U15_gaa(T163, T155, T154, leE_in_gag(T163, T155, false))
U15_gaa(T163, T155, T154, leE_out_gag(T163, T155, false)) → U16_gaa(T163, T155, T154, minusF_in_gaa(T163, s(T155), T154))
U16_gaa(T163, T155, T154, minusF_out_gaa(T163, s(T155), T154)) → minusF_out_gaa(s(T163), s(T155), s(T154))
MINUSF_IN_GAA(s(T163), s(T155), s(T154)) → U15_GAA(T163, T155, T154, leE_in_gag(T163, T155, false))
U15_GAA(T163, T155, T154, leE_out_gag(T163, T155, false)) → MINUSF_IN_GAA(T163, s(T155), T154)
leE_in_gag(s(T121), 0, false) → leE_out_gag(s(T121), 0, false)
leE_in_gag(s(T126), s(T128), X251) → U11_gag(T126, T128, X251, leE_in_gag(T126, T128, X251))
U11_gag(T126, T128, X251, leE_out_gag(T126, T128, X251)) → leE_out_gag(s(T126), s(T128), X251)
leE_in_gag(0, T116, true) → leE_out_gag(0, T116, true)
MINUSF_IN_GAA(s(T163)) → U15_GAA(T163, leE_in_gag(T163, false))
U15_GAA(T163, leE_out_gag) → MINUSF_IN_GAA(T163)
leE_in_gag(s(T121), false) → leE_out_gag
leE_in_gag(s(T126), X251) → U11_gag(leE_in_gag(T126, X251))
U11_gag(leE_out_gag) → leE_out_gag
leE_in_gag(0, true) → leE_out_gag
leE_in_gag(x0, x1)
U11_gag(x0)
From the DPs we obtained the following set of size-change graphs:
MINUSC_IN_GA(s(T94), s(T75)) → U9_GA(T94, T75, leD_in_gg(s(T94), false))
U9_GA(T94, T75, leD_out_gg(s(T94), false)) → MINUSC_IN_GA(T94, T75)
minusF_in_gaa(0, T25, 0) → minusF_out_gaa(0, T25, 0)
minusF_in_gaa(s(T44), 0, s(T38)) → U12_gaa(T44, T38, minusC_in_ga(T44, T38))
minusC_in_ga(T52, T54) → U5_ga(T52, T54, leD_in_ga(T52, X81))
leD_in_ga(0, true) → leD_out_ga(0, true)
leD_in_ga(s(T60), false) → leD_out_ga(s(T60), false)
U5_ga(T52, T54, leD_out_ga(T52, X81)) → minusC_out_ga(T52, T54)
minusC_in_ga(T68, 0) → U6_ga(T68, leD_in_gg(T68, true))
leD_in_gg(0, true) → leD_out_gg(0, true)
leD_in_gg(s(T60), false) → leD_out_gg(s(T60), false)
U6_ga(T68, leD_out_gg(T68, true)) → minusC_out_ga(T68, 0)
minusC_in_ga(0, s(T75)) → U7_ga(T75, leD_in_gg(0, false))
U7_ga(T75, leD_out_gg(0, false)) → U8_ga(T75, minusA_in_a(T75))
minusA_in_a(T82) → U1_a(T82, leB_in_a(X148))
leB_in_a(true) → leB_out_a(true)
U1_a(T82, leB_out_a(X148)) → minusA_out_a(T82)
minusA_in_a(0) → U2_a(leB_in_g(true))
leB_in_g(true) → leB_out_g(true)
U2_a(leB_out_g(true)) → minusA_out_a(0)
minusA_in_a(s(T87)) → U3_a(T87, leB_in_g(false))
U3_a(T87, leB_out_g(false)) → U4_a(T87, minusA_in_a(T87))
U4_a(T87, minusA_out_a(T87)) → minusA_out_a(s(T87))
U8_ga(T75, minusA_out_a(T75)) → minusC_out_ga(0, s(T75))
minusC_in_ga(s(T94), s(T75)) → U9_ga(T94, T75, leD_in_gg(s(T94), false))
U9_ga(T94, T75, leD_out_gg(s(T94), false)) → U10_ga(T94, T75, minusC_in_ga(T94, T75))
U10_ga(T94, T75, minusC_out_ga(T94, T75)) → minusC_out_ga(s(T94), s(T75))
U12_gaa(T44, T38, minusC_out_ga(T44, T38)) → minusF_out_gaa(s(T44), 0, s(T38))
minusF_in_gaa(s(T101), s(T103), T104) → U13_gaa(T101, T103, T104, leE_in_gaa(T101, T103, X225))
leE_in_gaa(0, T116, true) → leE_out_gaa(0, T116, true)
leE_in_gaa(s(T121), 0, false) → leE_out_gaa(s(T121), 0, false)
leE_in_gaa(s(T126), s(T128), X251) → U11_gaa(T126, T128, X251, leE_in_gaa(T126, T128, X251))
U11_gaa(T126, T128, X251, leE_out_gaa(T126, T128, X251)) → leE_out_gaa(s(T126), s(T128), X251)
U13_gaa(T101, T103, T104, leE_out_gaa(T101, T103, X225)) → minusF_out_gaa(s(T101), s(T103), T104)
minusF_in_gaa(s(T143), s(T144), 0) → U14_gaa(T143, T144, leE_in_gag(T143, T144, true))
leE_in_gag(0, T116, true) → leE_out_gag(0, T116, true)
leE_in_gag(s(T121), 0, false) → leE_out_gag(s(T121), 0, false)
leE_in_gag(s(T126), s(T128), X251) → U11_gag(T126, T128, X251, leE_in_gag(T126, T128, X251))
U11_gag(T126, T128, X251, leE_out_gag(T126, T128, X251)) → leE_out_gag(s(T126), s(T128), X251)
U14_gaa(T143, T144, leE_out_gag(T143, T144, true)) → minusF_out_gaa(s(T143), s(T144), 0)
minusF_in_gaa(s(T163), s(T155), s(T154)) → U15_gaa(T163, T155, T154, leE_in_gag(T163, T155, false))
U15_gaa(T163, T155, T154, leE_out_gag(T163, T155, false)) → U16_gaa(T163, T155, T154, minusF_in_gaa(T163, s(T155), T154))
U16_gaa(T163, T155, T154, minusF_out_gaa(T163, s(T155), T154)) → minusF_out_gaa(s(T163), s(T155), s(T154))
MINUSC_IN_GA(s(T94), s(T75)) → U9_GA(T94, T75, leD_in_gg(s(T94), false))
U9_GA(T94, T75, leD_out_gg(s(T94), false)) → MINUSC_IN_GA(T94, T75)
leD_in_gg(s(T60), false) → leD_out_gg(s(T60), false)
MINUSC_IN_GA(s(T94)) → U9_GA(T94, leD_in_gg(s(T94), false))
U9_GA(T94, leD_out_gg) → MINUSC_IN_GA(T94)
leD_in_gg(s(T60), false) → leD_out_gg
leD_in_gg(x0, x1)
From the DPs we obtained the following set of size-change graphs: